$\forall$$T$:Type, $L$:$T$ List, $a$:$T$, $P$:($T$$\rightarrow\mathbb{B}$).
\\[0ex]index{-}of{-}first $x$ in $a$.$L$.$P$($x$)
\\[0ex]$\sim$
\\[0ex]if $P$($a$)$\rightarrow$ 1 ; 0$<_{2}$index{-}of{-}first $x$ in $L$.$P$($x$)$\rightarrow$ index{-}of{-}first $x$ in $L$.$P$($x$)+1 else 0 fi